Nuprl Lemma : sender_wf 0,22

EX1X2:Type, info:(E(IdX1+(IdLnkE)X2)), e:E. rcv?(e sender(e E 
latex


Definitionsrcv?(e), sender(e), ecase1(e;info;i.f(i);l,e'.g(l;e')), x:AB(x), Id, IdLnk, b, False, P  Q, t  T, True
Lemmastrue wf, false wf, IdLnk wf, Id wf, rcv? wf, assert wf

origin